Inference at * 1 
Iof proof for Lemma fib wf:



1. n : 
2. n1:. (n1 < n)  (fib(n1)  )
  fib(n)   

latex

 by InteriorProof ((RecCaseSplit `fib`) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
CollapseTHENA ((Au),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: .....truecase..... NILNIL

C1: 3. (n = 0)  (n = 1)
C1:   1  
C2: .....falsecase..... NILNIL

C2: 3. ((n = 0)) & ((n = 1))
C2:   fib(n - 1)+fib(n - 2)  
C.

Definitions	T, ff, P  Q, P  Q, tt, if b then t else f fi , Y, fib(n), P  Q, x:A. B(x), True, P & Q, P  Q, , t  T, Unit, , ,
Lemmas	not functionality wrt iff, assert of bnot, and functionality wrt iff, assert of band, bnot thru bor, true wf, squash wf, eqff to assert, assert of eq int, or functionality wrt iff, assert of bor, eqtt to assert, iff transitivity, not wf, bnot wf, band wf, assert wf, bool wf, eq int wf, bor wf